ABS: a:A fp B(a)

STM: fpf wf

STM: subtype-fpf-general

STM: subtype-fpf

STM: subtype-fpf-variant

STM: subtype-fpf2

STM: subtype-fpf3

ABS: x  dom(f)

STM: fpf-dom wf

ABS: fpf-domain(f)

STM: fpf-domain wf

STM: member-fpf-domain

STM: member-fpf-domain-variant

STM: fpf-trivial-subtype-set

STM: fpf-trivial-subtype-top

STM: fpf-type

STM: fpf-dom functionality

STM: fpf-dom functionality2

STM: fpf-dom-type

STM: fpf-dom-type2

ABS: 

STM: fpf-empty wf

ABS: fpf-is-empty(f)

STM: fpf-is-empty wf

STM: assert-fpf-is-empty

ABS: f(x)

STM: fpf-ap wf

STM: fpf-ap functionality

ABS: f(x)?z

STM: fpf-cap-wf-univ

STM: fpf-cap wf

ABS: z != f(x)  P(a;z)

STM: fpf-val wf

ABS: f  g

STM: fpf-sub wf

STM: sq stable fpf-sub

STM: fpf-empty-sub

STM: fpf-sub-functionality

STM: fpf-sub-functionality2

STM: fpf-sub functionality

STM: fpf-sub functionality2

STM: fpf-sub transitivity

STM: fpf-sub weakening

STM: subtype-fpf-cap

STM: subtype-fpf-cap-top

STM: fpf-cap-void-subtype

STM: subtype-fpf-cap-void

STM: fpf-cap functionality

STM: fpf-cap-subtype functionality

STM: fpf-cap functionality wrt sub

STM: fpf-cap-subtype functionality wrt sub

STM: fpf-cap-subtype functionality wrt sub2

ABS: f || g

STM: fpf-compatible wf

STM: fpf-compatible-wf2

STM: fpf-sub-compatible-left

STM: fpf-sub-compatible-right

STM: subtype-fpf-cap5

STM: subtype-fpf-cap-void2

STM: subtype-fpf-cap-void-list

STM: fpf-cap-compatible

ABS: f  g

STM: fpf-join wf

STM: fpf-join-wf

STM: fpf-join-empty

STM: fpf-empty-join

STM: fpf-join-empty-sq

STM: fpf-join-idempotent

STM: fpf-join-assoc

STM: fpf-join-dom

STM: fpf-join-dom2

STM: fpf-join-dom-sq

STM: fpf-domain-join

STM: fpf-join-is-empty

STM: fpf-join-ap

STM: fpf-join-ap-left

STM: fpf-join-ap-sq

STM: fpf-join-cap-sq

STM: fpf-join-cap

STM: fpf-join-range

STM: fpf-sub-join-left

STM: fpf-sub-join-left2

STM: fpf-sub-join-right

STM: fpf-sub-join-right2

STM: fpf-sub-join

STM: fpf-join-sub

STM: fpf-join-sub2

ABS: (L)

STM: fpf-join-list wf

STM: fpf-join-list-dom

STM: fpf-join-list-dom2

STM: fpf-join-list-domain

STM: fpf-join-list-domain2

STM: fpf-join-list-ap

STM: fpf-join-list-ap2

STM: fpf-join-list-ap-disjoint

ABS: fpf join cons compseq tag def

ABS: fpf join nil compseq tag def

STM: fpf-sub-join-symmetry

STM: fpf-sub-val

STM: fpf-sub-val2

STM: fpf-sub-val3

ABS: L fpf v

STM: fpf-const wf

STM: fpf-const-dom

ABS: x : v

STM: fpf-single wf

STM: fpf-single wf2

STM: fpf-single wf3

STM: fpf-single-sub-reflexive

STM: fpf-cap-single1

STM: fpf-split

STM: fpf-cap-single-join

STM: fpf-ap-single

STM: fpf-cap-single

STM: fpf-val-single1

ABS: fx : v

STM: fpf-add-single wf

ABS: fpf-vals(eq;P;f)

STM: fpf-vals wf

STM: member-fpf-vals

STM: member-fpf-vals2

STM: filter-fpf-vals

STM: fpf-vals-singleton

STM: fpf-vals-nil

ABS: xdom(f). v=f(x)   P(x;v)

STM: fpf-all wf

ABS: fpf-map(a,v.f(a;v);x)

STM: fpf-map wf

ABS: fpf-accum(z,a,v.f(z;a;v);y;x)

STM: fpf-accum wf

ABS: rename(r;f)

STM: fpf-rename wf

STM: fpf-rename-dom

STM: fpf-rename-dom2

STM: fpf-rename-ap

STM: fpf-rename-ap2

STM: fpf-rename-cap

STM: fpf-rename-cap2

STM: fpf-rename-cap3

ABS: fpf-inv-rename(r;rinv;f)

STM: fpf-inv-rename wf

ABS: g o f

STM: fpf-compose wf

ABS: fpf dom compose compseq tag def

ABS: fpf ap compose compseq tag def

STM: fpf-dom-compose

STM: fpf-ap-compose

ABS: compose-fpf(a;b;f)

STM: compose-fpf wf

STM: compose-fpf-dom

STM: fpf-sub-reflexive

ABS: mkfpf(a;b)

STM: mkfpf wf

STM: fpf-join-compatible-left

STM: fpf-join-compatible-right

STM: fpf-compatible-self

STM: fpf-compatible-join

STM: fpf-compatible-join-iff

STM: fpf-compatible-symmetry

STM: fpf-disjoint-compatible

STM: fpf-compatible-update

STM: fpf-compatible-update2

STM: fpf-compatible-update3

STM: fpf-compatible-join2

STM: fpf-compatible-singles

STM: fpf-compatible-singles-trivial

STM: fpf-single-dom

STM: fpf-single-dom-sq

STM: fpf-compatible-single

STM: fpf-compatible-single-iff

STM: fpf-compatible-single2

STM: fpf-compatible-singles-iff

STM: fpf-decompose

STM: fpf-compatible-join-cap

STM: fpf-ap-equal

STM: fpf-join-dom-decl

STM: fpf-join-dom-da

STM: fpf-cap-join-subtype

STM: fpf-cap-join-subtype2

STM: fpf-all-empty

STM: fpf-all-single

STM: fpf-all-single-decl

STM: fpf-all-join-decl

ABS: non-void(d)

STM: non-void-decl wf

STM: non-void-decl-join

STM: non-void-decl-single

ABS: AtomFree(d)

STM: fpf-empty-compatible-right

STM: fpf-empty-compatible-left

STM: fpf-compatible-triple

ABS: fpf-dom-list(f)

STM: fpf-dom-list wf

STM: member-fpf-dom

ABS: lnk-decl(l;dt)

STM: lnk-decl wf

STM: lnk-decl-cap

STM: lnk-decl-dom

STM: lnk-decl-dom-single

STM: lnk-decl-dom-join

STM: lnk-decl-dom-not

STM: lnk-decl-dom2

STM: lnk-decl-cap2

STM: lnk-decl-ap

STM: lnk-decl-dom-implies

STM: lnk-decl-compatible-single

STM: lnk-decl-compatible-single2

STM: lnk-decls-compatible

STM: l disjoint-fpf-dom

STM: l disjoint-fpf-join-dom

ABS: fpf(L)

STM: pairs-fpf wf

STM: pairs-fpf property

STM: no repeats-pairs-fpf

ABS: fpf-normalize(eq;g)

STM: fpf-normalize wf

STM: fpf-normalize-dom

STM: fpf-normalize-ap

ABS: Valtype(da;k)

STM: ma-valtype wf

ABS: Msgtype(da;k)

STM: ma-msgtype wf

ABS: State(ds)

STM: ma-state wf

ABS: timedState(ds)

STM: ma-tstate wf

STM: ma-valtype-subtype

STM: ma-state-subtype

STM: ma-state-subtype2

ABS: dt(l;da)

STM: es-dt wf

STM: es-dt-dom

STM: es-dt-ap

STM: es-dt-cap

ABS: Normal(T)

STM: normal-type wf

STM: normal-top

ABS: Normal(ds)

STM: normal-ds wf

STM: implies-normal-ds

STM: normal-ds-single

STM: normal-ds-join

ABS: Normal(da)

STM: normal-da wf

STM: normal-da-single

STM: normal-da-join

STM: normal-valtype

STM: normal-cap-void

STM: normal-es-dt

STM: normal-p-outcome